VERIDIS - 2011 - Annual activity report

VERIDIS

VERIDIS - 2011

Team Veridis

Members

Overall Objectives

Introduction
Highlights

Scientific Foundations

Automated and interactive theorem proving
Methodology of proved system development

Application Domains

Application Domains

Software

The veriT solver
The TLA⁺ proof system

New Results

Using symmetries in SMT
Compression of SMT proofs
Combination of decision procedures
Encoding TLA⁺ proof obligations for SMT solvers
Model checking within SimGrid
A new version of PlusCal
Verification of distributed algorithms in the Heard-Of model
Modeling and verifying the Pastry routing protocol
Incremental development of distributed algorithms
Bounding message length in attacks against security protocols
Formally verified decision procedures for finite automata

Contracts and Grants with Industry

ANR project DeCert
Tools and Methodologies for Formal Specifications and for Proofs
Diagnosis of errors in network controlled systems

Partnerships and Cooperations

European Initiatives
International Initiatives

Dissemination

Animation of the scientific community
Teaching

Bibliography

Major publications
Publications of the year
References in notes

Previous |

Home | Next next

Section: Contracts and Grants with Industry

Tools and Methodologies for Formal Specifications and for Proofs

Participants : Stephan Merz, Hernán-Pablo Vanzetto.

We participate in the project on Tools and Methodologies for Formal Specifications and for Proofs at the MSR-INRIA Joint Centre. The objective of the project is to develop a proof environment for verifying distributed algorithms in TLA⁺ (see also sections 5.2 and 6.4 ). The project in particular funds the PhD thesis of Hernán Vanzetto.

Previous |

Home | Next next